Verification of a circuit design typically involves testing the circuit design before the design is physically implemented as a circuit (e.g., fabricated as an integrated circuit). In this way, errors (i.e. “bugs”) in the design may be identified before the designer incurs the expense of fabrication.
As circuit designs have become increasingly complex, the task of creating efficient and effective verification tools has become increasing difficult. For example, conventional system-on-chip designs may include relatively large, fast and complex integrated memories, on-chip buses, and sophisticated arbiters. Moreover, these designs typically involve concurrent processes many of which may be interdependent.
Stimulation-based tools have traditionally been used to verify designs. These tools typically verify a design by randomly applying tests to portions of the design. However, simulation-based validation methodologies often fail to discover corner-case design errors. An example of a corner-case error may include an error that does not occur until a specific set of conditions occur at the same time wherein that set of conditions occurs relatively infrequently.
Various formal analysis techniques (“formal techniques”) have been proposed for use in verification of circuit designs. The concept behind formal techniques is to thoroughly search the design for errors. Examples of formal techniques include model checking, theorem proving and symbolic simulation.
Applications of formal techniques include verifying a cache coherency protocol using a symbolic model checker and verifying commonly used design structures such as arithmetic circuits, pipelines, bus arbiters and Tomasulo's algorithm. Recently, formal techniques have been applied on a wider range of designs. For example, B. Bentley, Validating the Intel Pentium 4 microprocessor, In Design Automation Conference, pages 244-248, 2001, discusses the use of formal techniques to find over 100 “high-quality” logic bugs in the Pentium 4®.
Most formal techniques cannot, however, be applied efficiently to relatively large industrial designs. Some techniques have been proposed to address this problem, including symbolic algorithms, SAT procedures, and abstraction techniques, however, solutions to such problems remain a continuing need.